$\forall$${\it es}$:ES, $T$:Type, $c$:$T$, $i$, $x$:Id, $e$:E.
\\[0ex]@$i$ $x$ initially $c$:$T$ $\Rightarrow$ (loc($e$) = $i$) $\Rightarrow$ \{@$i$($x$:$T$) c$\wedge$ (($x$ when first{-}event\{i:l\}(${\it es}$;$e$)) = $c$)\}